i:Id, L:Knd List, l:IdLnk, tg:Id.
@i: only L sends on (l with tg) 
realizes es.
e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L) 

latex

Definitions	t  T, x:A. B(x)
Lemmas	not wf, assert wf, null wf3